Section: Partnerships and Cooperations

National Initiatives

• ANR programme blanc CPP (“Confidence, Probability, and Proofs”), 2009-2012. Partners: LSV (scientific leader), CEA LIST (co-leader), INRIA (Comète, Parsifal), Ecole Supérieure d'Electricité (L2S, SSE). External partners: Safran, Dassault Systèmes.

  In the context of proofs of safety properties for critical software, The CPP project proposes to study the joint use of probabilistic and formal (deterministic) semantics and analysis methods, in a way to improve the applicability and precision of static analysis methods on numerical programs. See http://www.lix.polytechnique.fr/~bouissou/cpp/index.php .

• ANR SeSur (“Sécurité et Sûreté Informatique”) project AVOTÉ, 2008-2012. Partners: INRIA (Cassis, leader), LSV, Verimag and, until September 2009 France Télécom R&D.

  Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes. However, the convenience of electronic elections comes with a risk of large-scale fraud and their security has seriously been questioned. The AVOTÉ project aims at proposing formal methods to analyze electronic voting protocols. See http://www.lsv.ens-cachan.fr/anr-avote/ .

• ANR VERSO program ProSe (“Proofs of Security”), 2010-2014. Partners: INRIA (Cascade, leader; Cassis), LSV, Verimag.

  The goal of the ProSe project is to increase the confidence in security protocols, and in order to reach this goal, provide security proofs at three levels: the symbolic level, in which messages are terms; the computational level, in which messages are bitstrings; and the implementation level: the program itself. This project is a continuation of the FormaCrypt project. See https://crypto.di.ens.fr/projects:prose:main .